;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(interface IFileReader
  (sig CharsToRat(chars))
  (sig RatToChars(rational decimals))
  (sig ExtractBetweenCommas (lineAsChars startComma endComma commaCount))
  (sig ExtractFromComma (lineAsChars startComma commaCount))
  (sig breakAtNextLine (fileAsChars))
  (sig stringToArgs (string))
  
  (con validExtractBetweenCommas
       (let* ((result (ExtractBetweenCommas (lineAsChars startComma endComma commaCount))))
         (implies (standard-char-listp lineAsChars) (standard-char-listp result))))
  
  (con validExtractFromComma 
       (let* ((result (ExtractFromComma(lineAsChars startComma commaCount))))
         (implies (standard-char-listp lineAsChars) (standard-char-listp result))))
  
  (con validBreakAtNextLine
       (let* ((result (breakAtNextLine (fileAsChars))))
         (implies (standard-char-listp lineAsChars) (standard-char-listp result)))))